T:Type, P1, P2:(T), L:(T List). filter(P1;filter(P2;L)) ~ filter(t.(P1(t))  (P2(t));L) 

latex

Definitions	T, P  Q, P  Q, P & Q, P  Q, b, True, b, p  q, , ff, tt, P  Q, if b then t else f fi , t  T, Y, reduce(f;k;as), filter(P;l), x:A. B(x), False, Unit, ,
Lemmas	or functionality wrt iff, assert of bor, bnot thru band, squash wf, true wf, btrue wf, bor wf, assert of band, bfalse wf, band wf, bool cases sqequal, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf